event{-}info(${\it ds}$;${\it da}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$k$:Knd $\times$ (:decl{-}state(${\it ds}$) $\times$ fpf{-}cap(${\it da}$; Kind{-}deq; $k$; top))